\begin{tabbing}
R{-}discrete($R$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=case $R$ of \+
\\[0ex]Rnone =$>$ $\otimes$
\\[0ex]Rplus(${\it left}$,${\it right}$)=$>$${\it rec}_{1}$,${\it rec}_{2}$.fpf{-}join(product{-}deq(Id;Id;IdDeq;IdDeq);${\it rec}_{1}$;${\it rec}_{2}$)
\\[0ex]Rinit(${\it loc}$,$T$,$x$,$v$)=$>$ $<$${\it loc}$, $x$$>$ : case $v$ of inl($a$) =$>$ tt $\mid$ inr($a$) =$>$ ff
\\[0ex]Rframe(${\it loc}$,$T$,$x$,$L$)=$>$ $\otimes$
\\[0ex]Rsframe(${\it lnk}$,${\it tag}$,$L$)=$>$ $\otimes$
\\[0ex]Reffect(${\it loc}$,${\it ds}$,${\it knd}$,$T$,$x$,$f$)=$>$ $<$${\it loc}$, $x$$>$ : case $f$ of inl($a$) =$>$ tt $\mid$ inr($a$) =$>$ ff
\\[0ex]Rsends(${\it ds}$,${\it knd}$,$T$,$l$,${\it dt}$,$g$)=$>$ $\otimes$
\\[0ex]Rpre(${\it loc}$,${\it ds}$,$a$,$T$,$P$)=$>$ $\otimes$
\\[0ex]Rkframe(${\it loc}$,$k$,$L$)=$>$ $\otimes$
\\[0ex]Rksframe(${\it loc}$,$k$,$L$)=$>$ $\otimes$
\\[0ex]Rrframe(${\it loc}$,$x$,$L$)=$>$ $\otimes$
\-
\end{tabbing}